ข้ามไปยังเนื้อหา

แท็ก

#Dependent Types

1 บทความ

Bend 2 มาแล้ว: ภาษาที่ให้คุณเขียน 'กฎ' แล้วบังคับให้ AI พิสูจน์ว่าโค้ดไม่ละเมิด — type checker เร็วกว่า Rocq 20 เท่า แต่ตัวเลขบนหน้าเว็บมีข้อควรอ่าน
เครื่องมือนักพัฒนา

Bend 2 มาแล้ว: ภาษาที่ให้คุณเขียน 'กฎ' แล้วบังคับให้ AI พิสูจน์ว่าโค้ดไม่ละเมิด — type checker เร็วกว่า Rocq 20 เท่า แต่ตัวเลขบนหน้าเว็บมีข้อควรอ่าน

16-17 ก.ย. ทีม HigherOrderCO ปล่อย Bend 2 ภายใต้ Apache-2.0 พร้อมแนวคิด LAWS.bend — ไฟล์ที่คุณประกาศกฎที่แอปห้ามละเมิด แล้ว compiler จะไม่ยอมให้ AI merge โค้ดจนกว่าจะพิสูจน์ได้ว่ากฎยังอยู่ ตัวเลข benchmark ในรีโปยืนยันว่า checker เร็วจริง (0.295 วิ เทียบ Rocq 5.985 วิ, Lean 36.177 วิ) แต่คำโฆษณา 'เร็วเท่า C บนคอร์เดียว' อ่านจาก pin ของเขาเองแล้วยังช้ากว่า C ใน 15 จาก 16 เบนช์

· อ่าน 8 นาที